package com.googlecode.kipler.satisfiability.interpolation.rule;

import java.util.Iterator;

import com.googlecode.kipler.container.dl.BasicWcsInterpolationData;
import com.googlecode.kipler.container.dl.LabelManager;
import com.googlecode.kipler.syntax.concept.ConceptName;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.Formula;

public class ClashInterpolantRule extends InterpolantRule {
	@Override
	public ConceptAssertion apply() {
		BasicWcsInterpolationData wcsData = (BasicWcsInterpolationData) getWcs()
				.getData();
		LabelManager labelMan = wcsData.getLabelManager();
		Iterator<Formula> fIter = getCondition().iterator();
		ConceptAssertion firstFormula = (ConceptAssertion) fIter.next();
		ConceptAssertion secondFormula = (ConceptAssertion) fIter.next();
		if (firstFormula.getConcept() instanceof ConceptName
				&& firstFormula.getConcept().isNegated()) {
			ConceptAssertion temp = firstFormula;
			firstFormula = secondFormula;
			secondFormula = temp;
		}
		boolean firstLabelLeft = labelMan.isLeftDerived(firstFormula);
		boolean secondLabelLeft = labelMan.isLeftDerived(secondFormula);
		ConceptAssertion result = new ConceptAssertion();
		result.setName(firstFormula.getName());
		if (firstLabelLeft && secondLabelLeft) {
			result.setConcept(ConceptName.bottomConcept());
		} else if (firstLabelLeft && !secondLabelLeft) {
			result.setConcept(firstFormula.getConcept());
		} else if (!firstLabelLeft && secondLabelLeft) {
			result.setConcept(secondFormula.getConcept());
		} else {
			result.setConcept(ConceptName.topConcept());
		}
		return result;
	}
}
